\chapter{Chang-Roberts leader election protocol}

\begin{quest}
	Given the provided encoding of the Chang-Roberts leader election protocol,
	prove that
	\begin{itemize}
		\item[(a)] after finishing successfully, the value of LEAD($i$) is the same
			for all nodes $i$ (show how many iterations are required in the corresponding
			analysis);
		\item[(b)] this resulting LEAD value is equal to the maximum of
			all UIDs;
		\item[(c)] no deadlock may occur, that is, as long as the system has not finished
			successfully, there is always at least one rule applicable.
	\end{itemize}
	Let $N$ be the number of nodes.
\end{quest}

\section{SMT solver and encoding}

For this problem, we used \textsc{bddsolve} because it involves reachability and essentially
only Boolean values. We represented the state of the system of nodes using the following
Boolean variables (Table \ref{tab:state-vars}) in the most straightforward way.

\begin{table}[htp]
	\centering
	\begin{tabular}{lll}
		\toprule[1.2pt]
		Variable & A.k.a     & Description \\
		\midrule
		$p_i$    & PART($i$) & participation of the $i$-th node \\
		$l_i$    & LA($i$)   & leader availability \\
		$m_i$    & MA($i$)   & message availability \\
		$s_{ik}$ & MESS($i$) & the message ($\lceil \log_2 N \rceil$ bits)\\
		$b_{ik}$ & LEAD($i$) & \emph{boss}: elected leader UID ($\lceil \log_2 N \rceil$ bits)\\
		\bottomrule[1.1pt]
	\end{tabular}
	\vspace{2mm}
	\caption{State variables; the index $i$ ranges over nodes in the system}
	\label{tab:state-vars}
\end{table}

\noindent For $N$ nodes, this yields $O(N \log N)$ bits of state. In particular, for 4 nodes we get 28
state bits. Without loss of generality, we assign nodes UIDs from the range $0 \ldots N-1$.

\subsection{Notation}

Throughout this text, we will use the following shortcut notation (Table \ref{tab:notation}).

\begin{table}[htp]
	\centering
	\begin{tabular}{lll}
		\toprule[1.2pt]
		Notation & Formalization & Description \\
		\midrule
		$x_i^t$  & --- & value $x$ of the node $i$ at the time $t$ \\
		\addlinespace[1.5mm]
		$x_i \equiv y_j$ & $\bigwedge_{0 \leq k < \lceil \log_2 N \rceil} x_{ik} = y_{jk}$
			& equality of bit sequences \\
		\addlinespace[1.5mm]
		$[x_1, \ldots, x_n] \trans [y_1, \ldots, y_n]$
			& $\bigwedge \{x_1\ldots x_n,y_1 \ldots y_n\}$
			& state transition rule \\
		\addlinespace[1.5mm]
		$x =^* n$ & $\sum x_i 2^i = n$ & $x$ is binary notation of the number $n$ \\
		\addlinespace[1.5mm]
		$x <^* n$ & $\sum x_i 2^i \leq n$ & $x$ represents a number $\leq n$ \\
		\bottomrule[1.1pt]
	\end{tabular}
	\vspace{2mm}
	\caption{Notation used}
	\label{tab:notation}
\end{table}

\section{Initial condition}

The initial condition is easy. The assignment says that initially,
all bits MA, LA, and PART are false.
\begin{equation}
	\label{eq:initial}
	\mathsf{initial} = \bigwedge_{i} \neg m_i \wedge \neg l_i \wedge \neg p_i
\end{equation}

\section{Transition}

\subsection{Concurrent semantics}

The assignment suggests full non-determinism (,,if $X$ then the node \emph{may} do $Y$'')
so there is no specific order of operation, nodes operate non-deterministically in parallel.
However, there is semantics to be chosen; namely, we need to resolve write-write and read-write
conflicts (nodes have read/write access to their neighbors' memory cells).

The simplest solution is to go with the stop-the-world semantics: we model nodes that take turns
(in an unspecified order), modifying the world state while all other nodes are sleeping, which
leads to atomicity of the actions performed by a single node in one ,,clock cycle''. We assume
that real-world nodes have hardware (or other) synchronization means to achieve such atomicity.

\subsection{Transition relation}

Now that our semantics is clear, the top-most transition relation is clear as well: in each clock
cycle/iteration, (exactly) one node ,,ticks''.
\begin{equation}
	\label{eq:transition}
	\mathsf{transition} = \bigvee_i \mathsf{tick}(i)
\end{equation}
The disjunction is actually exclusive; because of the definition of \textsf{tick}.
\begin{align*}
	\mathsf{tick}(i)
		&= \bigwedge_{i \neq j \neq n(i)} \mathsf{sleep}(j)
			& \text{(freeze other nodes)} \\
		&\quad\wedge \mathsf{passivate}(n(i)) 
			& \text{(passivate neighbor)} \\
		&\quad\wedge \big[ \mathsf{activate}(i) \vee \mathsf{pass}(i)
			\vee \mathsf{lead}(i) \vee \mathsf{end}(i) \big]
			& \text{(perform an action)}
\end{align*}
Now we need to introduce the subpredicates used in the tick predicate (recall Table \ref{tab:notation}
on page \pageref{tab:notation} for notation),
\begin{align}
	\mathsf{passivate}(i)
		&= (p_i^{t+1} = p_i^t) \wedge (b_i^{t+1} \equiv b_i^t) \\
	\mathsf{sleep}(i)
		&= \mathsf{passivate}(i) \wedge (m_i^{t+1} = m_i^t) \wedge (s_i^{t+1} \equiv s_i^t) \mint{,} \\
\intertext{along with the four possible node actions:}
	\begin{split}
	\mathsf{activate}(i) &= [\neg p_i^t, \neg l_i^t] \\
		&\trans [p_i^{t+1}, \neg l_i^{t+1}, b_i^{t+1} \equiv b_i^t,
			m_i^t = m_i^{t+1}, s_i^t \equiv s_i^{t+1},
			m_{n(i)}^{t+1}, s_{n(i)}^{t+1} =^* i,
			l_{n(i)}^{t+1} = l_{n(i)}^t]
	\end{split} \\
	\begin{split}
	\mathsf{pass}(i) &= [p_i^t, \neg l_i^t, m_i^t, s_i^t >^* i] \\
		&\trans [p_i^{t+1}, \neg l_i^{t+1}, b_i^{t+1} \equiv b_i^t,
			\neg m_i^{t+1}, s_i^t \equiv s_i^{t+1}, 
			m_{n(i)}^{t+1}, s_{n(i)}^{t+1} \equiv s_i^t,
			l_{n(i)}^{t+1} = l_{n(i)}^t]
	\end{split} \\
	\begin{split}
	\mathsf{lead}(i) &= [p_i^t, \neg l_i^t, m_i^t, s_i^t =^* i] \\
		&\trans [p_i^{t+1}, l_i^{t+1}, b_i^{t+1} \equiv b_i^t,
			\neg m_i^{t+1}, s_i^t \equiv s_i^{t+1}, 
			m_{n(i)}^{t+1} = m_{n(i)}^t, s_{n(i)}^{t+1} \equiv s_{n(i)}^t,
			l_{n(i)}^{t+1} = l_{n(i)}^t]
	\end{split} \\
	\begin{split}
	\mathsf{end}(i) &= [p_i^t, l_i^t] \\
		&\trans [\neg p_i^{t+1}, l_i^{t+1}, b_i^{t+1} \equiv b_i^t,
			\neg m_i^{t+1}, s_i^t \equiv s_i^{t+1}, 
			m_{n(i)}^{t+1}, s_{n(i)}^{t+1} \equiv s_i^t,
			l_{n(i)}^{t+1}]
	\end{split}
\end{align}
Please excuse the convoluted notation, it's essentially a literal encoding of the assignment. In the
\textsc{Haskell} code, these formulas are further factored into more suitably named subpredicates.
Here however, for the sake of brevity, we use raw formulas.

\section{Final condition}

Here we have to prove three claims about the above algorithm. This is most easily done by expressing
these claims as satisfiability problems, combining them in a suitable way so that the whole formula
is unsatisfiable if and only if these claims are true.

In other words, we want to find a state, where at least one of the following three conditions
are true:
\begin{itemize}
	\item[(a)] After successful end, the nodes have chosen different leaders;
	\item[(b)] after successful end, the leader is not the one with the maximum UID;
	\item[(c)] none of the rules are applicable before successful end.
\end{itemize}
If such a state is \emph{not} reachable, the algorithm satisfies the three correctness claims.
This is formalized as:
\begin{equation}
	\label{eq:final}
	\mathsf{final} = (\mathsf{success} \wedge \mathsf{inequalLeaders})
		\vee (\mathsf{success} \wedge \mathsf{nonMaxLeader})
		\vee (\neg \mathsf{success} \wedge \mathsf{deadlock})
\end{equation}
First, we need the happyend predicate
\begin{equation}
	\mathsf{success} = \bigvee_i l_i \wedge m_i \wedge \neg p_i \mint{,}
\end{equation}
which is followed by three core (in)correctness predicates:
\begin{align}
	\mathsf{inequalLeaders} &= \bigvee_{i < j} b_i \not \equiv b_j \\
	\mathsf{nonMaxLeader} &= \bigvee_{i} b_i \neq^* (N-1)
\end{align}
Note that the predicate \textsf{nonMaxLeader} subsumes \textsf{inequalLeaders}. For the sake of
simplicity, we will however keep the latter as well.

The last incorrectness predicate is a bit more involved; it checks the non-applicability (precondition)
of every transition rule (at every node).
\begin{equation}
\begin{split}
	\mathsf{deadlock} &= \bigwedge_i \mathsf{blocked}(i) \\
	\mathsf{blocked}(i) &=
		\neg ( \neg p_i \wedge \neg l_i ) \\
		&\wedge \neg ( p_i \wedge \neg l_i \wedge m_i \wedge s_i >^* i ) \\
		&\wedge \neg ( p_i \wedge \neg l_i \wedge m_i \wedge s_i =^* i ) \\
		&\wedge \neg ( p_i \wedge l_i )
\end{split}
\end{equation}

\section{Putting it all together}

We can finally construct the \textsc{bddsolve} program, using \textsf{initial} (Eq. \ref{eq:initial},
page \pageref{eq:initial}) as the initial state predicate, \textsf{transition}
(Eq. \ref{eq:transition}, page \pageref{eq:transition}) as the transition relation, and
\textsf{final} (Eq. \ref{eq:final}, page \pageref{eq:final}) as the final state predicate.

\subsection{Implementation and code}

The implementation\footnote{
\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/leader.hs}} was done using a
\textsc{Haskell} embedded domain-specific language, which generates \textsc{bddsolve} source code,
with use of the \textsc{reachability} logic.

\subsection{Answers}

\textsc{Bddsolve} reports the described formula as unsatisfiable, hence the three correctness
claims are true. The reported number of iterations searched by \textsc{bddsolve} is 12.

See Figure \ref{fig:bddsolve-leader} on page \pageref{fig:bddsolve-leader} for the output of 
\textsc{bddsolve} for the above problem.

\begin{figure}[ht]
\centering
\begin{minipage}{8.5cm}
\begin{verbatim}
iteration     bdd size     # reachable states
    0              12             65536
    1              58            131072
    2             122            155648
    3             170            163840
    4             194            166144
    5             209            167424
    6             217            167680
    7             225            167936
    8             229            168192
    9             246            168256
   10             263            168272
   11             282            168276
   12             303            168277


number of possible transitions   : 620756992
number of reachable final states : 0
0.01 seconds elapsed for solving reach problem
0 seconds elapsed for backtracking solution

REACH FAILED
\end{verbatim}
\end{minipage}
\caption{\textsc{Bddsolve} output for the described formula}
\label{fig:bddsolve-leader}
\end{figure}








































































